FDL - Nuprl Lemma : es-interface-local-pred-bool

Nuprl Lemma : es-interface-local-pred-bool

es:ES, P:(E

).

X:AbsInterface(E)

(

e:E.

((

(e

X))

(

a:E. (es-p-local-pred(es;

e.

(P(e)))(e,a))))

& ((

(e

X))

(es-p-local-pred(es;

e.

(P(e)))(e,X(e)))))

Definitions es-p-local-pred(es;P), AbsInterface(A), , x.A(x), A B, a < b, P Q, A, False, P & Q, P Q, left + right, strong-subtype(A;B), t T, E, ES, e(e1,e2].P(e), e[e1,e2].P(e), e[e1,e2].P(e), e[e1,e2).P(e), e[e1,e2).P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e<e'.P(e), e c e', (e < e'), e loc e' , (e <loc e'), l_disjoint(T;l1;l2), (x l), Outcome, q-rel(r;x), r < s, r s, (xL.P(x)), xL. P(x), x f y, f(a), A c B, a < b, a <p b, a b, a ~ b, b | a, x:A. B(x), x:A B(x), P Q, s = t, b, x:A. B(x), x:AB(x), Dec(P)

Lemmas decidable assert, decidable wf, assert wf, es-E wf, es-interface-local-pred, es-interface wf, iff wf, es-p-local-pred wf, bool wf, event system wf